/*
Copyright 2013 Nicola Olivetti, Gian Luca Pozzato. This file is part of NESCOND.NESCOND is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with NESCOND. If not, see <http://www.gnu.org/licenses/>.
*/

/* Automatic generator of formulas of NESCOND

To test the performances of NESCOND for CK and comparing them with the ones of CondLean and UCK,
run: 

  statistic(GoalVars,KBVars,DimKB,NumGoals,Depth,MSec)

Generated formulas have the form: A_1 ^ A_2 ^ É ^ A_n -> B (in order to be used also by the goal-directed UCK)
GoalVars=KBVars=number of different propositional variables
DimKB=n (i.e. number of conjuncts in the antecedent)
NumGoals= number of different Bs to use in the consequent
Depth=maximun level of nesting of formulas
MSec=timeout.

To run NESCOND on 88 valid formulas (obtained by translating modal K valid formulas from Heuerding-Beckert-GorŽ),
run:

statNS(MSec)

MSec=timeout.

To list K valid formulas, run:
listOfValidFormulas(List).

*/

:- op(400,fy,-), 
   op(500,xfy,&), 
   op(600,xfy,v), 
   op(700,xfy,<=>),
   op(400,fy,box), 
   op(400,fy,dia).


:- op(400,fy,neg), 
   op(500,xfy,and), 
   op(600,xfy,or),
   op(650,xfy,->), 
   op(450,xfy,=>).
   
:-use_module(library(random)).
:-use_module(library(lists)).
:-use_module(library(timeout)).

genD(ATM,Var,0):-!,length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genD(ATM,Fml,Depth):-random(1,4,Rand),Depth1 is Depth - 1,genDIn(ATM,Rand,Fml,Depth1).
genDIn(ATM,1,true -> Var,_):-length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genDIn(ATM,2,(G) -> (Var),Depth):-length(ATM,L),L1 is L+1,random(1,L1,Position),
  nth(Position,ATM,Var),genG(ATM,G,Depth).
genDIn(ATM,3,(A) => (D),Depth):-genA(ATM,A,Depth),genD(ATM,D,Depth).

genG(ATM,Var,0):-!,length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genG(ATM,Fml,Depth):-random(1,6,Rand),Depth1 is Depth - 1,genGIn(ATM,Rand,Fml,Depth1).
genGIn(ATM,1,Var,_):-length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genGIn(_,2,true,_).
genGIn(ATM,3,(G1) and (G2),Depth):-genG(ATM,G1,Depth),genG(ATM,G2,Depth).
genGIn(ATM,4,(G1) or (G2),Depth):-genG(ATM,G1,Depth),genG(ATM,G2,Depth).
genGIn(ATM,5,(A) => (G),Depth):-genA(ATM,A,Depth),genG(ATM,G,Depth).


genA(ATM,Var,0):-!,length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genA(ATM,Fml,Depth):-random(1,4,Rand),Depth1 is Depth - 1,genAIn(ATM,Rand,Fml,Depth1).
genAIn(ATM,1,Var,_):-length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genAIn(ATM,2,(A1) and (A2),Depth):-genA(ATM,A1,Depth),genA(ATM,A2,Depth).
genAIn(ATM,3,(A1) or (A2),Depth):-genA(ATM,A1,Depth),genA(ATM,A2,Depth).


generateKnowledgeBase(0,_,[],_):-!.
generateKnowledgeBase(Dim,ATM,[[x,Fml]|KB],Depth):-genD(ATM,Fml,Depth),                                   
			           Dim1 is Dim-1,
                                   generateKnowledgeBase(Dim1,ATM,KB,Depth).
      
     
generatePropVars(1,[p]):-!.                                   
generatePropVars(2,[p,q]):-!.                                   
generatePropVars(3,[p,q,r]):-!.                                   
generatePropVars(4,[p,q,r,p1]):-!.                                   
generatePropVars(5,[p,q,r,p1,q1]):-!.                                   
generatePropVars(6,[p,q,r,p1,q1,r1]):-!.                                   
generatePropVars(7,[p,q,r,p1,q1,r1,p2]):-!.                                   
generatePropVars(8,[p,q,r,p1,q1,r1,p2,q2]):-!.                                   
generatePropVars(9,[p,q,r,p1,q1,r1,p2,q2,r2]):-!.     

/* Where are they now? */
subset(_,0,[]):-!.
subset([H|Tail],N,[H|ResTail]):-N1 is N-1,subset(Tail,N1,ResTail).                              
nth(1,[Head|_],Head):-!.
nth(N,[_|Tail],Res):-N1 is N-1,nth(N1,Tail,Res).


statistic(GoalVars,KBVars,DimKB,NumGoals,Depth,MSec):-
  retractall(successes(_)),
  retractall(timeouts(_)),
  retractall(succLean(_)),
  retractall(timeLean(_)),
  retractall(succNS(_)),
  retractall(timeNS(_)),
  asserta(successes(0)),
  asserta(timeouts(0)),
  asserta(succLean(0)),
  asserta(timeLean(0)),
  asserta(succNS(0)),
  asserta(timeNS(0)),
  generatePropVars(KBVars,ATM),
  subset(ATM,GoalVars,GoalATM),
  generateKnowledgeBase(DimKB,ATM,KB,Depth),
  listOfGoals(GoalATM,Goals,NumGoals,Depth),
/*  write('KB: '),
  write(KB),
  write('\nGOALS: '),
  write(Goals),
  write('\n'), */
  executeUCK(KB,Goals,MSec),
  successes(N),
  timeouts(T),
  write('ESECUZIONE UCK\n'),
  write(N),
  write(' successi su '),
  write(NumGoals),
  write(' prove\n'),
  write(T),
  write(' timeouts, '),
  F is NumGoals-N-T,
  write(F),
  write(' sequenti non validi\n'),
  write('ESECUZIONE CondLean\n'),
  executeCondLean(KB,Goals,MSec),
  succLean(NL),
  timeLean(TL),
  write(NL),
  write(' successi su '),
  write(NumGoals),
  write(' prove\n'),
  write(TL),
  write(' timeouts, '),
  FL is NumGoals-NL-TL,
  write(FL),
  write(' sequenti non validi\n'), 
  createNestedSequent(KB,NS),
  executeNested(NS,Goals,MSec),
  succNS(NNS),
  timeNS(TNS),
  write('ESECUZIONE implementazione nested sequents\n'),
  write(NNS),
  write(' successi su '),
  write(NumGoals),
  write(' prove\n'),
  write(TNS),
  write(' timeouts, '),
  FNS is NumGoals-NNS-TNS,
  write(FNS),
  write(' sequenti non validi\n'),
  write('Riassunto:          S   T   N\n'),
  write('UCK                  '),write(N),write('  '),write(T),write('  '),write(F),write('\n'),
  write('CondLean             '),write(NL),write('  '),write(TL),write('  '),write(FL),write('\n'),
  write('Nested sequents      '),write(NNS),write('  '),write(TNS),write('  '),write(FNS),write('\n').
  
  
listOfGoals(_,[],0,_):-!.
listOfGoals(ATM,[Goal|Tail],N,Depth):-genG(ATM,Goal,Depth),N1 is N-1,listOfGoals(ATM,Tail,N1,Depth).

executeUCK(_,[],_):-!.
executeUCK(KB,[Goal|Tail],MSec):-
  (
  time_out(proveU([x,Goal],KB,[],[x]),MSec,Result),!,
  (
    (
    Result=success,!,
    successes(N),retractall(successes(_)),N1 is N+1,asserta(successes(N1)),
    executeUCK(KB,Tail,MSec)
    );
    (
    timeouts(T),retractall(timeouts(_)),T1 is T+1,asserta(timeouts(T1)),
    executeUCK(KB,Tail,MSec)
    )
  )
  )
  ;
  executeUCK(KB,Tail,MSec).

executeCondLean(_,[],_):-!.
executeCondLean(KB,[Goal|Tail],MSec):-
  (
  time_out(
    (
      struttura(KB,LitSigma,TransSigma,LabSigma),
      struttura([[x,Goal]],LitDelta,TransDelta,LabDelta),
      proveCondLean([LitSigma,TransSigma,LabSigma],[LitDelta,TransDelta,LabDelta],[x])
    ),MSec,Result),!,
  (
    (
    Result=success,!,
    succLean(N),retractall(succLean(_)),N1 is N+1,asserta(succLean(N1)),
    executeCondLean(KB,Tail,MSec)
    );
    (
    timeLean(T),retractall(timeLean(_)),T1 is T+1,asserta(timeLean(T1)),
    executeCondLean(KB,Tail,MSec)
    )
  )
  )
  ;
  executeCondLean(KB,Tail,MSec). 


executeNested(_,[],_):-!.
executeNested(Fml,[Goal|Tail],MSec):-
  (
  time_out(
    (
      proveNS([Fml -> Goal])
    ),MSec,Result),!,
  (
    (
    Result=success,!,
    succNS(N),retractall(succNS(_)),N1 is N+1,asserta(succNS(N1)),
    executeNested(Fml,Tail,MSec)
    );
    (
    timeNS(T),retractall(timeNS(_)),T1 is T+1,asserta(timeNS(T1)),
    executeNested(Fml,Tail,MSec)
    )
  )
  )
  ;
/*  write('Fallimento su '),
  write(Fml -> Goal),
  write('\n'),*/
  executeNested(Fml,Tail,MSec). 


/* ---------------------------------------------------------------- */
/* ---------------------------------------------------------------- */

/* The following predicates implement UCK 1.0 */

/* ---------------------------------------------------------------- */
/* ---------------------------------------------------------------- */

proveU([_,true],_,_,_):-!.
proveU([X,Q],Gamma,_,_):-atom(Q),member([X,Q],Gamma),!.

/* Rules */
proveU([X,G1 and G2],Gamma,Trans,Labels):-
  proveU([X,G1],Gamma,Trans,Labels),!,
  proveU([X,G2],Gamma,Trans,Labels).
  
proveU([X,G1 or G2],Gamma,Trans,Labels):-
  (proveU([X,G1],Gamma,Trans,Labels),!);proveU([X,G2],Gamma,Trans,Labels).
  
proveU([X,A => G],Gamma,Trans,Labels):-  
  generaLabels(Y,Labels),
  proveU([Y,G],Gamma,[[X,A,Y]|Trans],[Y|Labels]).
  
proveU([X,A,Y],_,Trans,_):-
  member([X,AP,Y],Trans),
  flat(A,DefA),
  flat(AP,DefAP),
  proveU([x,A],DefAP,[],[x]),
  proveU([x,AP],DefA,[],[x]).
  
proveU([X,Q],Gamma,Trans,Labels):-
  member([X,G->Q],Gamma),
  atom(Q),
  proveU([X,G],Gamma,Trans,Labels).

proveU([X,Q],Gamma,Trans,Labels):-
  member([Y,F=>(G->Q)],Gamma),
  atom(Q),
  proveU([X,G],Gamma,Trans,Labels),
  extract(F,List),
  proveList(X,Y,List,Gamma,Trans,Labels).


/* Predicate implementing the flattening of a conjunction of formulas */
flat(P,[[x,P]]):-atom(P),!.
flat(A1 and A2,Res):-flat(A1,FlatA1),flat(A2,FlatA2),append(FlatA1,FlatA2,Res).

/* Auxiliary predicates to compute Uprop */
extract(Rest=>A,[A|Tail]):-!,extract(Rest,Tail).
extract(F,[F]):-!.
proveList(K,Y,[A],Gamma,Trans,Labels):-
  proveU([Y,A,K],Gamma,Trans,Labels).
proveList(X,Y,[A|Tail],Gamma,Trans,Labels):-
  proveU([K,A,X],Gamma,Trans,Labels),
  proveList(K,Y,Tail,Gamma,Trans,Labels).


/* -------------------------------------------------------------- */

/* This predicate generates a "new" label for that branch */
generaLabels(x,Labels):-true,\+member(x,Labels),!.
generaLabels(y,Labels):-true,\+member(y,Labels),!.
generaLabels(z,Labels):-true,\+member(z,Labels),!.
generaLabels(u,Labels):-true,\+member(z,Labels),!.
generaLabels(v,Labels):-true,\+member(z,Labels),!.
generaLabels(w,Labels):-true,\+member(z,Labels),!.
generaLabels(k,Labels):-true,\+member(k,Labels),!.
generaLabels(j,Labels):-true,\+member(j,Labels),!.
generaLabels(i,Labels):-true,\+member(i,Labels),!.
generaLabels(x+1,[i|_]):-!.
generaLabels(x+N1,[Last|_]):-Last=x+N,N1 is N+1,!.



/* ---------------------------------------------------------------- */
/* ---------------------------------------------------------------- */

/* The following predicates implement CondLean 3.1 */

/* ---------------------------------------------------------------- */
/* ---------------------------------------------------------------- */

/* Axioms */
/* true and false */
proveCondLean([LitSigma,_,_],_,_):-
  member([_,false],LitSigma),!.
proveCondLean(_,[LitDelta,_,_],_):-
  member([_,true],LitDelta),!.
proveCondLean([LitSigma,_,_],[LitDelta,_,_],_):-
  member(F,LitSigma),member(F,LitDelta),!.
proveCondLean([_,TransSigma,_],[_,TransDelta,_],_):-
  member(F,TransSigma),member(F,TransDelta),!.
proveCondLean([_,_,ComplexSigma],[_,_,ComplexDelta],_):-
  member(F,ComplexSigma),member(F,ComplexDelta),!.

/* Rules */
/* and L */
proveCondLean([LitSigma,TransSigma,ComplexSigma],Delta,Labels):-
  select([X,A and B],ComplexSigma,ResComplexSigma),!,
  put([X,A],LitSigma,ResComplexSigma,TempLitSigma,TempComplexSigma),
  put([X,B],TempLitSigma,TempComplexSigma,NewLitSigma,NewComplexSigma),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],Delta,Labels).
/* or R */
proveCondLean(Sigma,[LitDelta,TransDelta,ComplexDelta],Labels):-
  select([X,A or B],ComplexDelta,ResComplexDelta),!,
  put([X,A],LitDelta,ResComplexDelta,TempLitDelta,TempComplexDelta),
  put([X,B],TempLitDelta,TempComplexDelta,NewLitDelta,NewComplexDelta),
  proveCondLean(Sigma,[NewLitDelta,TransDelta,NewComplexDelta],Labels).
/* neg R */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],
    Labels):-
  select([X,neg A],ComplexDelta,ResComplexDelta),!,
  put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ResComplexDelta],Labels).
/* neg L */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels)
  :-select([X,neg A],ComplexSigma,ResComplexSigma),!,
  put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
  proveCondLean([LitSigma,TransSigma,ResComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Labels).
/* -> R */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels)
  :-select([X,A -> B],ComplexDelta,ResComplexDelta),!,
  put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
  put([X,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Labels).
/* => R */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels)
  :-select([X,A => B],ComplexDelta,ResComplexDelta),!,
  generaLabels(Y,Labels),
  put([Y,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta),
  proveCondLean([LitSigma,[[X,A,Y]|TransSigma],ComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],
    [Y|Labels]).
/* and R */
proveCondLean(Sigma,[LitDelta,TransDelta,ComplexDelta],Labels):-
  select([X,A and B],ComplexDelta,ResComplexDelta),!,
  put([X,A],LitDelta,ResComplexDelta,FirstLitDelta,FirstComplexDelta),
  put([X,B],LitDelta,ResComplexDelta,SecLitDelta,SecComplexDelta),
  proveCondLean(Sigma,[FirstLitDelta,TransDelta,FirstComplexDelta],Labels),
  proveCondLean(Sigma,[SecLitDelta,TransDelta,SecComplexDelta],Labels).
/* or L */
proveCondLean([LitSigma,TransSigma,ComplexSigma],Delta,Labels):-
  select([X,A or B],ComplexSigma,ResComplexSigma),!,
  put([X,A],LitSigma,ResComplexSigma,FirstLitSigma,FirstComplexSigma),
  put([X,B],LitSigma,ResComplexSigma,SecLitSigma,SecComplexSigma),
  proveCondLean([FirstLitSigma,TransSigma,FirstComplexSigma],Delta,Labels),
  proveCondLean([SecLitSigma,TransSigma,SecComplexSigma],Delta,Labels).
/* -> L */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels):-
  select([X,A -> B],ComplexSigma,ResComplexSigma),!,
  put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
  put([X,B],LitSigma,ResComplexSigma,NewLitSigma,NewComplexSigma),
  proveCondLean([LitSigma,TransSigma,ResComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Labels),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels).
/* => L  */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels):-
  select([X,A => B],ComplexSigma,ResComplexSigma),
  member([X,A_1,Y],TransSigma),
  proveCondLean([[],[[X,A_1,Y]],[]],[[],[[X,A,Y]],[]],Labels),
  put([Y,B],LitSigma,ResComplexSigma,NewLitSigma,NewComplexSigma),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ComplexDelta],
    Labels).
/* EQ */
proveCondLean([_,TransSigma,_],[_,TransDelta,_],_):-
  member([X,A,Y],TransSigma),member([X,B,Y],TransDelta),
  /* The premises are "independent" from the conclusion, so we can use label x
     for their proofs */
  put([x,A],[],[],FirstLitSigma,FirstComplexSigma),
  put([x,B],[],[],FirstLitDelta,FirstComplexDelta),
  put([x,B],[],[],SecLitSigma,SecComplexSigma),
  put([x,A],[],[],SecLitDelta,SecComplexDelta),
  proveCondLean([FirstLitSigma,[],FirstComplexSigma],[FirstLitDelta,[],FirstComplexDelta],
    [x]),
  proveCondLean([SecLitSigma,[],SecComplexSigma],[SecLitDelta,[],SecComplexDelta],
    [x]).


/* --------------------------------------------------------------------------------------- */


/* This predicate finds all the labels in the sequent 
      etichette(+Sequente,-ListaEtichette) */
etichette([],[]):-!.
etichette([[L,_]|Tail],[L|TailLab]):-etichette(Tail,TailLab),\+member(L,TailLab),!.
etichette([[L,_,L]|Tail],[L|TailLab]):-etichette(Tail,TailLab),\+member(L,TailLab),!.
etichette([[L1,_,L2]|Tail],[L1,L2|TailLab]):-etichette(Tail,TailLab),
  \+member(L1,TailLab),\+member(L2,TailLab),!.
etichette([[L1,_,L2]|Tail],[L1|TailLab]):-etichette(Tail,TailLab),
  \+member(L1,TailLab),member(L2,TailLab),!.
etichette([[L1,_,L2]|Tail],[L2|TailLab]):-etichette(Tail,TailLab),
  \+member(L2,TailLab),member(L1,TailLab),!.
etichette([_|Tail],Labels):-etichette(Tail,Labels).

/* This predicate creates a partition of the sequent in atomic, transition and complex formulas */
struttura([],[],[],[]):-!.
struttura([[X,A and B]|Tail],Literal,Transaction,[[X,A and B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A or B]|Tail],Literal,Transaction,[[X,A or B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A -> B]|Tail],Literal,Transaction,[[X,A -> B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A => B]|Tail],Literal,Transaction,[[X,A => B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,neg A]|Tail],Literal,Transaction,[[X,neg A]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A,Y]|Tail],Literal,[[X,A,Y]|TransTail],Formulae):-
  struttura(Tail,Literal,TransTail,Formulae),!.
struttura([X|Tail],[X|LitTail],Transition,Formulae):-
  struttura(Tail,LitTail,Transition,Formulae),!.

/* This predicate inserts a formula in the correct list; more precisely, a formula
   can be an atomic formula or a complex formula */
put([X,A and B],Literal,Formulae,Literal,[[X,A and B]|Formulae]):-!.
put([X,A or B],Literal,Formulae,Literal,[[X,A or B]|Formulae]):-!.
put([X,A -> B],Literal,Formulae,Literal,[[X,A -> B]|Formulae]):-!.
put([X,A => B],Literal,Formulae,Literal,[[X,A => B]|Formulae]):-!.
put([X,neg A],Literal,Formulae,Literal,[[X,neg A]|Formulae]):-!.
put(X,Literal,Formulae,[X|Literal],Formulae):-!.




/* Nested sequent calculi */
removeLabels([],[]):-!.
removeLabels([[_,Fml]|Tail],[Fml|ResTail]):-removeLabels(Tail,ResTail).
createConj([Singleton],Singleton):-!.
createConj([Head|Tail],Head and FmlTail):-createConj(Tail,FmlTail).
createNestedSequent(KB,Fml):-removeLabels(KB,KBUnlab),createConj(KBUnlab,Fml).


fillTheHole(NS,ListToFill,NewNS):-select(hole,NS,TempNS),!,
								  append(TempNS,ListToFill,NewNS).
fillTheHole(NS,ListToFill,[[[Fml,NewGamma],AppliedConditionals]|TempNS]):-select([[Fml,Gamma],AppliedConditionals],NS,TempNS),
								  fillTheHole(Gamma,ListToFill,NewGamma).

selectList([],NS,[hole|NS]).
selectList([Fml|Tail],NS,NewNS):-select(Fml,NS,TempNS),
								 selectList(Tail,TempNS,NewNS).
						
deepSelect(List,NS,NewNS):-selectList(List,NS,NewNS).
deepSelect(List,NS,[[[Fml,NewGamma],AppliedConditionals]|NewNS]):-select([[Fml,Gamma],AppliedConditionals],NS,NewNS),
						   deepSelect(List,Gamma,NewGamma).

memberList([],_):-!.
memberList([Head|Tail],NS):-member(Head,NS),memberList(Tail,NS).
deepMember(List,NS):-memberList(List,NS),!.
deepMember(List,NS):-member([[_,Gamma],_],NS),
					 deepMember(List,Gamma),!.

/* Axioms closing branches */
proveNS(NS):-deepMember([P,neg P],NS),!.
proveNS(NS):-deepMember([true],NS),!.
proveNS(NS):-deepMember([neg false],NS),!.
/* Rules with one premise */
proveNS(NS):-deepSelect([neg neg A],NS,NewNS),!,fillTheHole(NewNS,[A],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A or B],NS,NewNS),!,fillTheHole(NewNS,[A,B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([neg (A and B)],NS,NewNS),!,fillTheHole(NewNS,[neg A,neg B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A -> B],NS,NewNS),!,fillTheHole(NewNS,[neg A,B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A => B],NS,NewNS),!,fillTheHole(NewNS,[[[A,[B]],[]]],DefNS),proveNS(DefNS).
/* Rules with two or three premises (introducing a branch in a backward proof search) */
proveNS(NS):-deepSelect([neg (A or B)],NS,NewNS),!,fillTheHole(NewNS,[neg A],NS1),fillTheHole(NewNS,[neg B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-deepSelect([A and B],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-deepSelect([neg (A -> B)],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[neg B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-
    deepSelect([neg (A => B),[[C,Delta],AppliedConditionals]],NS,NewNS),
    \+member(neg (A => B),AppliedConditionals),!,
    proveNS([A,neg C]),
    proveNS([C,neg A]),
    fillTheHole(NewNS,[neg(A => B),[[C,[neg B|Delta]],[neg (A => B)|AppliedConditionals]]],DefNS),
    proveNS(DefNS).


statNS(Ms):-
  write('...loading examples...\n'),
  listOfValidFormulas(ListModLean),
  write('...DONE...\n'),
  write('...converting modal formulas...\n'),
  convertList(ListModLean,ListCond),
  write('...DONE...\n'),
  retractall(succ(_)),
  retractall(to(_)),
  retractall(fail(_)),
  retractall(listFail(_)),
  asserta(succ(0)),
  asserta(to(0)),
  asserta(fail(0)),
  asserta(listFail(0)),
  statList(ListCond,Ms),
  succ(NS),
  to(NTO),
  fail(NF),
  listFail(ListOfFail),
  write('Fallimento su: '),
  write(ListOfFail),
  write('\n\n'),
  write('Succ    TO    No \n'),
  write(NS),write('       '),
  write(NTO),write('       '),
  write(NF),write('\n').

statList([],_):-!.
statList([[Label,Fml]|Tail],Ms):-(
  time_out(
    (
      proveNS([neg (Fml)])
    ),Ms,Result),!,
  (
    (
    Result=success,!,
    succ(N),retractall(succ(_)),N1 is N+1,asserta(succ(N1)),
    statList(Tail,Ms)
    );
    (
    to(T),retractall(to(_)),T1 is T+1,asserta(to(T1)),
    statList(Tail,Ms)
    )
  )
  )
;
(
  fail(NF),
  listFail(LF),
  retractall(fail(_)),
  retractall(listFail(_)),
  N1 is NF+1,
  asserta(fail(N1)),
  asserta(listFail([Label|LF])),
  statList(Tail,Ms)
	).

convertList([],[]):-!.
convertList([[Label,_,Fml]|Tail],[[Label,ConvFml]|ResTail]):-convertFml(Fml,ConvFml),convertList(Tail,ResTail).
convertFml(-A,neg (CA)):-!,convertFml(A,CA).
convertFml(A & B,CA and CB):-!,convertFml(A,CA),convertFml(B,CB).
convertFml(A v B,CA or CB):-!,convertFml(A,CA),convertFml(B,CB).
convertFml(A -> B,CA -> CB):-!,convertFml(A,CA),convertFml(B,CB).
convertFml(box A,true => CA):-!,convertFml(A,CA).
convertFml(dia A,neg (true => neg (CA))):-!,convertFml(A,CA).
convertFml(P,P):-!.

listOfValidFormulas([
    [t1,2,-((box(p -> q)) -> ((box p) -> (box q)))],
    [t2,2,-(((box(p & q))) -> ((box p) & (box q)))],
	[t3,2,-(((box p) & (box (p -> q))) -> (box q))],
    [t4,2,-((((box p) & (dia (-q))) -> (dia (p & (-q)))))],
    [t5,2,-((((dia p) v (dia q)) -> (dia(p v q))))],
    [t6,2,(-(((box(p -> q)) -> ((box p) -> (box q))) &
	           (((box(p & q))) -> ((box p) & (box q))) & 
	           (((box p) & (box (p -> q))) -> (box q)) &
	           ((((box p) & (dia (-q))) -> (dia (p & (-q))))) &
	           ((((dia p) v (dia q)) -> (dia(p v q))))))],
    [raj6e1a1, 3, ((box (q v -(p))) & (box (p) & box (box q) & box (box
	                    q)) & dia -(p) & dia -(q))],  
    [raj6e1a2, 3, ((box (q v -(p))) & (box (p) & box (box q) & box (p))
	                    & dia -(p) & dia -(q))],
    [raj6e1b, 3, ((box (q v -(p))) & (box (p) & box (box p) & box (p v
	                    box q)) & dia -(p) & dia -(q))],
     [lwb4, 40, -(box p1 v box p2 v box p3 v box p5 v (dia (-p1 & box
	                p3) v dia (-p1 & box p5) v dia (-p2 & box p1) v (dia
	                (-p3 & box p3) v dia (-p3 & box p5)) v (dia (-p5 & box
	                p3) v dia (-p5 & box p5)) v (dia dia (-p1 & box p1) v
	                dia dia (-p1 & box p3) v dia dia (-p1 & box p4) v dia
	                dia (-p1 & box p5)) v (dia (-p4 & box p2) v dia (-p6 &
	                box p2)) v (dia dia (-p3 & box p1) v dia dia (-p3 &
	                box p3) v dia dia (-p3 & box p5)) v (dia (-p4 & box
	                p4) v dia (-p6 & box p4)) v (dia dia (-p5 & box p1) v
	                dia dia (-p5 & box p3) v dia dia (-p5 & box p5)) v
	                (dia (-p4 & box p6) v dia (-p6 & box p6)) v (dia dia
	                dia (-p1 & box p3) v dia dia dia (-p1 & box p5)) v
	                (dia dia (-p2 & box p2) v dia dia (-p4 & box p2) v dia
	                dia (-p6 & box p2)) v (dia dia dia (-p3 & box p3) v
	                dia dia dia (-p3 & box p5)) v (dia dia dia (-p4 & box
	                p1) v (dia dia (-p2 & box p4) v dia dia (-p4 & box p4)
	                v dia dia (-p6 & box p4))) v (dia dia dia (-p5 & box
	                p3) v dia dia dia (-p5 & box p5)) v (dia dia (-p2 &
	                box p6) v dia dia (-p4 & box p6) v dia dia (-p6 & box
	                p6)) v (dia dia dia (-p2 & box p2) v dia dia dia (-p6
	                & box p2)) v (dia dia dia (-p2 & box p4) v dia dia dia
	                (-p6 & box p4)) v (dia dia dia (-p2 & box p6) v dia
	                dia dia (-p6 & box p6))) v (dia dia dia dia -p2 v dia
	                dia dia dia -p4 v dia dia dia dia -p1 v dia dia dia
	                dia -p6))],
    [tx1,10,-((box p -> dia p) -> dia true)],
    [tx2,10,-((dia true -> box p -> dia p))],
    [tx3,10,-((box p -> box box p) -> box p & dia q -> dia (box p & q))],
    [tx4,10,-((box p & dia -box p -> dia (box p & -box p)) -> box p ->
	              box box p)],
    [tx5,10,-((dia p -> box dia p) -> dia p & dia q -> dia (dia p & q))],
    [tx6,10,-((dia p & dia -dia p -> dia (dia p & -dia p)) -> dia p ->
	              box dia p)],
    [tx7,10,-((p -> box dia p) -> p & dia q -> dia (dia p & q))],
    [tx8,10,-((p & dia -dia p -> dia (dia p & -dia p)) -> p -> box dia p)],
    [tx9,10,-((box false -> false) -> box p -> dia p)],
    [tx10,10,-((box dia -p -> dia -p) & (dia box p -> box dia box p) &
	               box (dia -p -> box dia -p) -> box p -> box box p)],
    [tx11,10,-((box -p -> -p) & (dia p -> box dia p) -> p -> box dia p)],
    [tx12,10,-((box (box -p -> box box -p) & (dia p -> box dia dia p)
	               -> dia p -> box dia p))],
    [tx13,10,-((box (dia -p -> box dia -p) & (box p -> box dia box p)
	               -> box p -> box box p))],
    [tx14,10,-((box p -> dia p) & (box p -> box box p) & (-p -> box dia
	               -p) -> box p -> p)],
    [tx15,10,-((dia box q -> box dia q) -> dia (p & box q) -> box (p v
	               dia q))],
    [tx16,10,-((box (box p -> dia p) & (dia (box p & box p) -> box (box
	               p v dia p)) -> dia box p -> box dia p))],
    [tx17,3,-((box (p & box p -> q) v box (q & box q -> p) -> box (p v
	               q) & box (box p v q) & box (p v box q) -> box p v box q))],
    [tx18,10,-((box ((p & box p -> q) v (q & box q -> p)) & box (box (p
	               & box p -> q) v (q & box q -> p)) & box ((p & box p ->
	               q) v box (q & box q -> p)) -> box (p & box p -> q) v
	               box (q & box q -> p)) -> box (p & box p -> q) v box (q
	               & box q -> p))],
    [tx19,10,-((box (box p -> q) v box (box q -> p) -> box (box p v q)
	               & box (p v box q) -> box p v box q))],
    [tx20,10,-((box (box (box p -> q) v (box q -> p)) & box ((box p ->
	               q) v box (box q -> p)) -> box (box p -> q) v box (box q
	               -> p)) -> box (box p -> q) v box (box q -> p))],
    [tx21,10,-((box (box p -> q) v box (box q -> p) -> box (p & box p
	               -> q) v box (q & box q -> p)))],
    [tx22,10,-((box (box p -> p) & box (box q -> q) & (box (p & box p
	               -> q) v box (q & box q -> p)) -> box (box p -> q) v box
	               (box q -> p)))],
    [tx23,10,-((box (box p -> p) & box (box q -> q) & (box (box p ->
	               box q) v box (box q -> box p)) -> box (box p -> q) v
	               box (box q -> p)))],
    [tx24,10,-((box (p & box p -> q) -> box box (p & box p -> q)) &
	               (box (q & box q -> p) -> box box (q & box q -> p)) &
	               box (box p -> box box p) & box (box q -> box box q) &
	               (box (p & box p -> q) v box (q & box q -> p)) -> box
	               (box p -> box q) v box (box q -> box p))],
    [tx25,10,-((dia box p -> box dia box p) & box (dia -p -> box dia
	               -p) -> box (box p -> box q) v box (box q -> box p))],
    [tx26,10,-((box (box -p -> dia -p) & (box (box p -> box -p) v box
	               (box -p -> box p)) -> dia box p -> box dia p))],
    [tx27,5,-((dia p -> box dia p) & (dia -p -> box dia -p) -> dia box
	               p -> box dia p)],
    [tx28,10,-((box (box dia p -> dia box p) -> box dia p -> dia box p)
	               & box (box p -> box box p) & box (box dia p -> dia box
	               p) -> dia box (p -> box p))],
    [tx29,10,-((box dia box (p -> box p) -> dia box (p -> box p)) &
	               (box dia -p -> box box dia -p) & dia box (p -> box p)
	               -> box dia p -> dia box p)],
    [tx30,20,-((box (dia q & (-p v -q)) -> box box (dia q & (-p v -q)))
	               & (box dia p -> dia box p) -> box dia p & box dia q ->
	               dia (p & q))],
    [tx31,10,-((box dia p & box dia -p -> dia (p & -p)) -> box dia p ->
	               dia box p)],
    [tx32,10,-((box dia p -> dia box p) -> box p -> dia p)],
    [tx33,10,-((box ((p v dia p) & (-p v dia -p)) -> box box ((p v dia
	               p) & (-p v dia -p))) & box (box (p & (p v dia p) & (-p
	               v dia -p)) -> box box (p & (p v dia p) & (-p v dia
	               -p))) & box (box (-p & (p v dia p) & (-p v dia -p)) ->
	               box box (-p & (p v dia p) & (-p v dia -p))) & (box dia
	               p -> dia box p) -> box (p v dia p) -> dia (p & box
	               p))],
    [tx34,10,-((box (p v dia p) -> dia (p & box p)) -> box dia p -> dia
	               box p)],
    [tx35,10,-((box (box (p & box p) -> p & box p) -> box (p & box p))
	               -> box p -> box box p)],
    [tx36,10,-((box (box false -> false) -> box false) -> box dia true
	               -> box false)],
    [tx37,10,-((box (box p -> p) -> box p) -> box (box p -> p) -> dia
	               box p -> box p)],
    [tx38,10,-((box dia true -> box false) & (box (box p -> p) -> dia
	               box p -> box p) -> box (box p -> p) -> box p)],
    [tx39,10,-((box (box (p & box (box p -> p)) -> p & box (box p ->
	               p)) -> box (p & box (box p -> p))) & box box (box (box
	               p -> p) -> box p) -> box (box (p -> box p) -> p) -> box
	               p)],
    [tx40,10,-((box (box p -> box box p) & (box (box p -> p) -> dia box
	               p -> box p) -> box (box (p -> box p) -> p) -> dia box p
	               -> box p))],
    [tx41,10,-((box (box (p -> box p) -> p) -> box box (box (p -> box
	               p) -> p)) & box (box p -> box box p) & (box (box (p ->
	               box p) -> p) -> dia box p -> p) & (box (box ((p -> box
	               p) -> box (p -> box p)) -> p -> box p) -> dia box (p ->
	               box p) -> p -> box p) -> box (box (p -> box p) -> p) ->
	               dia box p -> box p)],
    [tx42,10,-((box p -> p) & (box (box (p -> box p) -> p) -> dia box p
	               -> box p) -> box (box (p -> box p) -> p) -> dia box p
	               -> p)],
    [tx43,10,-((box (box p -> p) & (box (box (p -> box p) -> p) -> dia
	               box p -> p) -> box (box (p -> box p) -> box p) -> dia
	               box p -> p))],
    [tx44,10,-((box (box (box (p -> box p) -> box p) -> dia box p -> p)
	               -> box (box (p -> box p) -> box p) -> dia box p -> p) &
	               box (box (p -> box p) -> p -> box p) & box (box (box (p
	               -> box p) -> box p) -> dia box p -> p) -> box (box (p
	               -> box p) -> p) -> dia box p -> p)],
    [tx45,20,-((box (box p -> p) & (box (box (p -> box p) -> p) -> box
	               box (box (p -> box p) -> p)) & box (box p -> box box p)
	               & (box (box (p -> box p) -> p) -> dia box p -> p) &
	               (box (box ((p -> box p) -> box (p -> box p)) -> p ->
	               box p) -> dia box (p -> box p) -> p -> box p) -> box
	               (box (p -> box p) -> box p) -> dia box p -> box p))],
    [tx46,10,-((box p -> p) & (box (box (box (p -> box p) -> box p) ->
	               dia box p -> box p) -> box (box (p -> box p) -> box p)
	               -> dia box p -> box p) & box (box (p -> box p) -> p ->
	               box p) & box (box (box (p -> box p) -> box p) -> dia
	               box p -> box p) -> box (box (p -> box p) -> p) -> dia
	               box p -> p)],
    [tx47,10,-((box (box (p -> box p) -> p) -> dia box p -> p) -> box
	               (box (p -> box p) -> p) -> dia box p -> p v box p)],
    [tx48,10,-((box p -> p) & (box (box (p -> box p) -> p) -> dia box p
	               -> p v box p) -> box (box (p -> box p) -> p) -> dia box
	               p -> p)],
    [tx49,10,-((box (box ((box (p -> box p) -> p) & (box (box (p -> box
	               p) -> p) -> box box (box (p -> box p) -> p)) -> box
	               ((box (p -> box p) -> p) & (box (box (p -> box p) -> p)
	               -> box box (box (p -> box p) -> p)))) -> (box (p -> box
	               p) -> p) & (box (box (p -> box p) -> p) -> box box (box
	               (p -> box p) -> p))) -> (box (p -> box p) -> p) & (box
	               (box (p -> box p) -> p) -> box box (box (p -> box p) ->
	               p))) & box (box (box (p -> box p) -> p) -> p) -> box
	               (box (p -> box p) -> p) -> box p)],
    [tx50,10,-((box p -> p) & (box (box (box (p -> box p) -> p) -> box
	               p) -> box (box (p -> box p) -> p) -> box p) & box (box
	               (box (p -> box p) -> p) -> box p) -> box (box (p -> box
	               p) -> p) -> p)],
    [tx51,10,-((box (box (p -> box p) -> p) -> p) & box (box (box (p ->
	               box p) -> p) -> p) -> box (box (p -> box p) -> box p)
	               -> p)],
    [tx52,10,-((box (box (p -> box p) -> p -> box p) & (box -box (box
	               (p -> box p) -> p) -> -box (box (p -> box p) -> p)) &
	               (box (box (p -> box p) -> box p) -> p) -> box (box (p
	               -> box p) -> p) -> p))],
    [tx53,10,-((box (box ((box (p -> box p) -> box p) & (box (box (p ->
	               box p) -> p) -> p) & (box ((box (p -> box p) -> box p)
	               & (box (box (p -> box p) -> p) -> p)) -> box box ((box
	               (p -> box p) -> box p) & (box (box (p -> box p) -> p)
	               -> p))) -> box ((box (p -> box p) -> box p) & (box (box
	               (p -> box p) -> p) -> p) & (box ((box (p -> box p) ->
	               box p) & (box (box (p -> box p) -> p) -> p)) -> box box
	               ((box (p -> box p) -> box p) & (box (box (p -> box p)
	               -> p) -> p))))) -> (box (p -> box p) -> box p) & (box
	               (box (p -> box p) -> p) -> p) & (box ((box (p -> box p)
	               -> box p) & (box (box (p -> box p) -> p) -> p)) -> box
	               box ((box (p -> box p) -> box p) & (box (box (p -> box
	               p) -> p) -> p)))) -> (box (p -> box p) -> box p) & (box
	               (box (p -> box p) -> p) -> p) & (box ((box (p -> box p)
	               -> box p) & (box (box (p -> box p) -> p) -> p)) -> box
	               box ((box (p -> box p) -> box p) & (box (box (p -> box
	               p) -> p) -> p)))) & box (box (box (p -> box p) -> p) ->
	               p) -> box (box (p -> box p) -> box p) -> box p)],
    [tx54,10,-((box p -> p) & box (box (p -> box p) -> p -> box p) &
	               (box (box (p -> box p) -> box p) -> box p) -> box (box
	               (p -> box p) -> p) -> p)],
    [tx55,10,-((box (box (p -> box p) -> p) -> p) & (box (box ((box (p
	               -> box p) -> p) & (box (box (p -> box p) -> p) -> box
	               box (box (p -> box p) -> p)) -> box ((box (p -> box p)
	               -> p) & (box (box (p -> box p) -> p) -> box box (box (p
	               -> box p) -> p)))) -> (box (p -> box p) -> p) & (box
	               (box (p -> box p) -> p) -> box box (box (p -> box p) ->
	               p))) -> (box (p -> box p) -> p) & (box (box (p -> box
	               p) -> p) -> box box (box (p -> box p) -> p))) -> box
	               (box (p -> box p) -> p) -> p v box p)],
   [tx56,10,-((box p -> p) & (box (box (box (p -> box p) -> p) -> p v
	               box p) -> box (box (p -> box p) -> p) -> p v box p) &
	               box (box (box (p -> box p) -> p) -> p v box p) -> box
	               (box (p -> box p) -> p) -> p)],
   [tx57,30,-((box (box ((box (p -> box q) -> box q) & (box (box (p ->
	               box q) -> box q) -> box box (box (p -> box q) -> box
	               q)) -> box ((box (p -> box q) -> box q) & (box (box (p
	               -> box q) -> box q) -> box box (box (p -> box q) -> box
	               q)))) -> (box (p -> box q) -> box q) & (box (box (p ->
	               box q) -> box q) -> box box (box (p -> box q) -> box
	               q))) -> (box (p -> box q) -> box q) & (box (box (p ->
	               box q) -> box q) -> box box (box (p -> box q) -> box
	               q))) & (box (box ((box ((p -> box q) -> box (p -> box
	               q)) -> p -> box q) & (box (box ((p -> box q) -> box (p
	               -> box q)) -> p -> box q) -> box box (box ((p -> box q)
	               -> box (p -> box q)) -> p -> box q)) -> box ((box ((p
	               -> box q) -> box (p -> box q)) -> p -> box q) & (box
	               (box ((p -> box q) -> box (p -> box q)) -> p -> box q)
	               -> box box (box ((p -> box q) -> box (p -> box q)) -> p
	               -> box q)))) -> (box ((p -> box q) -> box (p -> box q))
	               -> p -> box q) & (box (box ((p -> box q) -> box (p ->
	               box q)) -> p -> box q) -> box box (box ((p -> box q) ->
	               box (p -> box q)) -> p -> box q))) -> (box ((p -> box
	               q) -> box (p -> box q)) -> p -> box q) & (box (box ((p
	               -> box q) -> box (p -> box q)) -> p -> box q) -> box
	               box (box ((p -> box q) -> box (p -> box q)) -> p -> box
	               q))) & box (box (box ((p -> box q) -> box (p -> box q))
	               -> p -> box q) -> p -> box q) -> box (box (p -> box q)
	               -> box q) & box (box (-p -> box q) -> box q) -> box
	               q)],
     [tx58,10,-((box (box (p -> box p) -> p) -> box (p -> box p) -> p) &
	               box box (box (p -> box p) -> p -> box p) & (box (box (p
	               -> box p) -> p) -> box box (box (p -> box p) -> p)) &
	               box (box p -> box box p) & (box (box (p -> box (p ->
	               box p)) -> box (p -> box p)) & box (box (-p -> box (p
	               -> box p)) -> box (p -> box p)) -> box (p -> box p)) ->
	               box (box (p -> box p) -> p) -> p)],
    [tx59,10,-((box (box (p -> box p) -> p) -> p) -> box p -> p)],
    [tx60,10,-((box (box (p & (box p -> box box p) -> box (p & (box p
	               -> box box p))) -> p & (box p -> box box p)) -> p &
	               (box p -> box box p)) -> box p -> box box p)],
    [tx61,10,-((box (box (dia -p -> box dia -p) -> dia -p) -> dia -p) &
	               (box (box (dia -p & (box dia -p -> box box dia -p) ->
	               box (dia -p & (box dia -p -> box box dia -p))) -> dia
	               -p & (box dia -p -> box box dia -p)) -> dia -p & (box
	               dia -p -> box box dia -p)) & (box (box (-box (p -> box
	               p) & (box -box (p -> box p) -> box box -box (p -> box
	               p)) -> box (-box (p -> box p) & (box -box (p -> box p)
	               -> box box -box (p -> box p)))) -> -box (p -> box p) &
	               (box -box (p -> box p) -> box box -box (p -> box p)))
	               -> -box (p -> box p) & (box -box (p -> box p) -> box
	               box -box (p -> box p))) & box (box (box (p -> box p) ->
	               p) -> p) -> box dia p -> dia box p)],
    [tx62,10,-((box (box (p -> box p) -> p) -> p) -> box (box (p -> box
	               p) -> p) -> dia box p -> p)],
    [tx63,10,-((box (box (p -> box p) -> p) -> box p) -> box (box (p ->
	               box p) -> p) -> dia box p -> box p)],
    [tx64,10,-((box (box -p -> -p) & (box dia p -> dia box p) & (box
	               (box (p -> box p) -> p) -> dia box p -> p) -> box (box
	               (p -> box p) -> p) -> p))],
    [tx65,10,-((dia box (box p -> q) -> (box p -> q) -> box (box p ->
	               q)) -> box (box p -> q) v box (box q -> p))],
    [tx66,10,-((box dia box p -> dia box p) & (dia box p -> p -> box p)
	               -> box dia box p -> p -> box p)],
    [tx67,10,-((box box (box (box p -> box box p) -> box p -> box box
	               p) & box box (box -(box dia box p & box p) -> -(box dia
	               box p & box p)) & box (box p -> box box p) & (box (box
	               dia box p -> -box p) v box (box -box p -> dia box p)) &
	               (box dia box p -> p -> box p) -> dia box p -> p -> box
	               p))],
    [tx68,10,-((box dia p -> dia p) & box (box -box dia p -> -box dia
	               p) & (box dia p -> box box dia p) & box (dia box dia p
	               -> p -> box p) -> box dia p -> dia box p)],
    [tx69,10,-((box box (box -p -> -p) & (dia box dia p -> p -> box p)
	               -> dia box p -> p -> box p))],
    [tx70,10,-((box -box p -> box box -box p) & box (box dia p -> dia
	               box p) & (dia box p -> p -> box p) -> dia box dia p ->
	               p -> box p)],
    [tx71,10,-((box box box (box p -> p) & (dia box dia p -> p -> box
	               p) & box (dia box dia -p -> -p -> box -p) -> p -> box
	               (dia p -> p)))],
    [tx72,10,-((box (box (p -> box p) -> p) -> box (p -> box p) -> p) &
	               box (box (p & (box (p -> box p) -> p)) -> box box (p &
	               (box (p -> box p) -> p))) & (dia box (p -> box p) -> (p
	               -> box p) -> box (p -> box p)) -> box (box (p -> box p)
	               -> p) -> dia box p -> p)],
			    [raj6c11, 4, ((box (-(p) v dia-(p))) & (box (p v q) & box (box p v
				                   q) & box (p v box q)) & dia -(q))],
			    [raj6c1, 4, ((box (-(p) v dia-(p))) & (box (p v q & r) & box (box p
				                v q) & box (p v box q)) & dia -(p) & dia -(q))],
							    [lwb1, 1, -(box p1 v box p2 v box p3 v box p5 v false v (dia -p2 v
								               dia -p4 v dia -p2 v dia -p6))],
										    [lwb2, 13, -(box p1 v box p2 v box p3 v box p5 v (dia (-p1 & box
											                p1) v dia (-p1 & box p3) v dia (-p2 & box p5) v (dia
											                (-p3 & box p1) v dia (-p3 & box p3)) v (dia (-p5 & box
											                p1) v dia (-p5 & box p3)) v (dia (-p4 & box p2) v dia
											                (-p6 & box p2)) v (dia (-p4 & box p4) v dia (-p6 & box
											                p4)) v (dia (-p4 & box p6) v dia (-p6 & box p6))) v
											                (dia dia -p2 v dia dia -p4 v dia dia -p5 v dia dia
											                -p6))],
														   [lwb3, 53, -(box p1 v box p2 v box p3 v box p5 v (dia (-p1 & box
															                p1) v dia (-p1 & box p3) v dia (-p2 & box p5) v (dia
															                (-p3 & box p1) v dia (-p3 & box p3)) v (dia (-p5 & box
															                p1) v dia (-p5 & box p3)) v (dia dia (-p1 & box p1) v
															                dia dia (-p1 & box p3) v dia dia (-p1 & box p5)) v
															                (dia (-p4 & box p2) v dia (-p6 & box p2)) v (dia dia
															                (-p3 & box p1) v dia dia (-p3 & box p3) v dia dia (-p3
															                & box p5)) v (dia (-p4 & box p4) v dia (-p6 & box p4))
															                v (dia dia (-p5 & box p1) v dia dia (-p5 & box p3) v
															                dia dia (-p5 & box p2) v dia dia (-p5 & box p5)) v
															                (dia (-p4 & box p6) v dia (-p6 & box p6)) v (dia dia
															                (-p2 & box p2) v dia dia (-p4 & box p2) v dia dia (-p6
															                & box p2)) v (dia dia (-p2 & box p4) v dia dia (-p4 &
															                box p4) v dia dia (-p6 & box p4)) v (dia dia (-p2 &
															                box p6) v dia dia (-p4 & box p6) v dia dia (-p6 & box
															                p6))) v (dia dia dia -p2 v dia dia dia -p4 v dia dia
															                dia -p2 v dia dia dia -p6))],
				[raj6c,2, ((box (-(p) v dia-(p))) & (box (p v q) & box (box p v q)) & dia -(p) & dia (-q))]
	]).